-- None of the functions and type defined in this module
-- should be exported anymore
module Pfla.PeanoNumerals() where
import Prelude hiding (pred)

data Zero = Zero
data Succ a = Succ a

data UnknownSize = UnknownSize

type One = Succ Zero
type Two = Succ One
type Three = Succ Two

zero = undefined :: Zero
one = undefined :: One
two = undefined :: Two
three = undefined :: Three

pred :: Succ a -> a
pred = undefined

class Cardinal a where
    cardToInt :: a -> Int

instance Cardinal Zero where
    cardToInt _ = 0

instance (Cardinal a) => Cardinal (Succ a) where
    cardToInt x = 1 + (cardToInt $ pred x)

instance Cardinal UnknownSize where
    cardToInt _ = -1
-- Use case:

data SList size a = SList [a]
    deriving Show

buildSListDynamic :: [a] -> SList c a
buildSListDynamic = \xs -> SList xs

buildSList :: (Cardinal c) => c -> [a] -> SList c a
buildSList size xs
    |   cardToInt size == -1 || (cardToInt size) == (length xs) = SList xs 
    |   otherwise = error "Size mismatch"

szip :: SList size a -> SList size b -> SList size (a,b)
szip (SList xs) (SList ys) = SList (zip xs ys)
